1. Technical Field
The present invention is directed to an apparatus and method for automated use of phase abstraction for enhanced verification of circuit designs.
2. Description of Related Art
Functional hardware verification is the process of demonstrating the correct behavior of a hardware design. Typically, the verification is performed on a xe2x80x9csoftwarexe2x80x9d model of the design, e.g., the hardware description language (HDL), or a netlist representation derived through compilation of the HDL or custom design (or some other xe2x80x9ccompiledxe2x80x9d format), which is executed on a computer or downloaded onto a hardware emulator. A trace of the xe2x80x9csoftwarexe2x80x9d model is generated by a verification tool and may be used to expose any problems in the software model or provide an output to a human user that may use the trace to evaluate the correctness of the design during operation.
A trace may be, for example, an xe2x80x9call events tracexe2x80x9d that illustrates 0, 1 valuations to each gate of a software model over time. Such traces can be created by simulation tools evaluating the software model in response to a test case, e.g., sequences of 0, 1 values of the input to the software model over time, or by formal verification algorithms which are commonly referred to as xe2x80x9ccounterexample traces.xe2x80x9d
The size of the design under test represents a significant bottleneck for the necessary verification resources. For simulation and emulation test-based techniques, the required resources are nearly linear with respect to design size. The drawback of such test-based techniques is that they are incomplete, and cannot prove the absence of design flaws, only their presence. Consequently there has been a peak of interest in formal verification techniques, which can prove the absence as well as presence of design flaws. However, such techniques consume exponential verification resources with respect to design size. In particular, verification resources typically run exponential with respect to the number of sequential elements (e.g., latches or registers) in the design. Combinational optimization techniques, prevalent in both test-based and formal verification paradigms, are capable of significantly reducing design size, but are limited in applicability to only the logic between sequential element boundaries. Thus sequential elements limit the ability of combinational model reduction techniques to simplify designs for verification regardless of the verification paradigm.
One technique, known as phase abstraction, has been developed to help minimize the number of sequential elements in a design under test. The use of phase abstraction for enhanced verification has been noted in several publications including xe2x80x9cEfficient Equivalence Checking of Multi-Phase Designs Using Phase Abstraction and Retiming,xe2x80x9d G. Hasteer, A. Mathur, and P. Banerjee, in Proceedings of the High-Level Design Validation and Test Symposium 1997 (which focusses on sequential hardware equivalence checking) and xe2x80x9cModel Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High-Performance Netlists,xe2x80x9d J. Baumgartner, T. Heyman, V. Singhal, and A. Aziz, in Proceedings of the Conference on Computer-Aided Verification 1999 (which focusses on functional verification), which are hereby incorporated by reference. In addition, a specific technique for performing phase abstraction is described in commonly assigned U.S. Pat. No. 6,321,184, which is also hereby incorporated by reference. In particular, for a design composed of level-sensitive latches, phase abstraction converts all but one xe2x80x9cclassxe2x80x9d of latches to wires based on the fact that the latches are transparent when they are clocked. The remaining class of latches is converted to registers, thereby significantly reducing the number of sequential elements by at least a factor of xe2x80x9ckxe2x80x9d for a xe2x80x9ckxe2x80x9d-phase design.
The impact of this technique on increasing the power of combinational optimization techniques, and on increasing the speed with which verification algorithms operate (basically linear for test-based techniques, and exponential for formal verification techniques), has been previously noted above. However, this technique has several complications and unpleasant side effects.
First, one must provide the glue to partition the latches into various classes. In other words, the user of the phase abstraction technique must identify which latches are of a particular type in order for the phase abstraction to work. Thus, an additional burden is placed on the user of the phase abstraction technique. Moreover, if the determination of latch type is incorrect, verification of the phase abstracted netlist becomes unsound, i.e. the verification results obtained on the phase abstracted netlist may not imply anything about correctness of the original netlist.
Second, design techniques such as gated-clock latches provide complications for these techniques. During phase abstraction, if a gated clock latch is replaced by a wire, the resulting trace includes errors due to the fact that the latch is not always transparent during the latch""s clocking at which it is normally transparent. This is because a gate signal may be used to alter the operation of the latch during this clocking. In particular, the global clock of the netlist can be selectively stopped for gated-clock latches by ANDing this global clock with a gate signal before driving it to these latches. As a result, if phase abstraction eliminates such latches, their gated behavior is destroyed, i.e. when their gates xe2x80x9cclosexe2x80x9d they will still appear to behave as if their gates were xe2x80x9copen.xe2x80x9d Thus, phase abstraction in the presence of gated-clock latches also risks making the transformation unsound for verification purposes.
Third, any simulation-style of traces obtained on a phase abstracted design will be in terms of the phase-abstracted model itself, which may be unattractive to those who expect a trace in terms of the original model. It may be difficult and time consuming for the human user of the phase abstraction technique to convert the trace obtained through phase abstraction into a corresponding trace that would have been obtained without the phase abstraction.
Thus, it would be beneficial to have an apparatus and method for eliminating these three unattractive side-effects and/or complications of phase abstraction and thereby, provide a truly seamless or xe2x80x9cinvisiblexe2x80x9d automatic use of phase abstraction for enhanced verification.
The present invention provides an apparatus and method for automated use of phase abstraction for enhanced verification of circuit designs. With the apparatus and method of the present invention latches are xe2x80x9ccolored,xe2x80x9d i.e. classified into different types, based on information obtained from a clock tree of the circuit design. In the clock tree, clock tree primitives drive all clock signals to the latches. These clock tree primitives contain sufficient information to taxonomize the clocks into their respective phases. This information may further be used to identify which latches are gated latches.
In coloring the latches, in a preferred embodiment, gated latches are replaced in the circuit design with a free running clock, a multiplexor, and a sequence of L1 to Ln latches to provide a feedback path via the data path. This allows the gated latch to be phase abstracted without losing the xe2x80x9cgatedxe2x80x9d functionality of the gated latch in the resulting trace.
Once the latches are colored in this way, phase abstraction is performed on the colored circuit design. The phase abstracted netlist is then subjected to verification, e.g., simulation, or formal verification. As a result of the verification, a trace may be produced. This trace will be in terms of the phase abstracted circuit, since verification was performed upon the phase abstracted circuit. The coloring information of the original circuit, plus information as to the exact nature of the phase abstraction performed, is then used to transform the phase abstracted trace to one which resembles a trace of the circuit without phase abstraction.
To undo the effects of phase abstraction in the trace, a list of all signal names of each xe2x80x9ccolorxe2x80x9d is generated. In other words, all nets are colored such that all nets combinationally driven by latches of color xe2x80x9cixe2x80x9d also have color xe2x80x9cixe2x80x9d; all nets combinationally driving data_in of latches of color xe2x80x9cixe2x80x9d have color xe2x80x9c(ixe2x88x921) mod kxe2x80x9d; all nets in combinational cones of color xe2x80x9cixe2x80x9d also have color xe2x80x9cixe2x80x9d; and all non-clock nets not colored by the above are defaulted to color xe2x80x9c0xe2x80x9d. Having colored the nets and generated a listing of all signals, the effects of the phase abstraction are removed from the phase-abstracted trace by propagating only signals appearing in the xe2x80x9ccolor_ixe2x80x9d list, i.e. clock tree signals are eliminated; and for a color xe2x80x9cjxe2x80x9d signal, the value present in the phase-abstracted trace at time xe2x80x9cixe2x80x9d will be replicated at times xe2x80x9ck*ixe2x88x92jxe2x80x9d through xe2x80x9ck*(i+1)xe2x88x92jxe2x88x921.xe2x80x9d Note that xe2x80x9cjxe2x80x9d ranges from 0 to kxe2x88x921.
These and other features and advantages of the present invention will be described in, or will become apparent to those of ordinary skill in the art in view of, the following detailed description of the preferred embodiments.